(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const v15 Bool)
(declare-const v16 Bool)
(declare-const v17 Bool)
(declare-const v18 Bool)
(declare-const v20 Bool)
(declare-const v21 Bool)
(declare-const _20-0 (_ BitVec 20))
(assert v6)
(assert (=> v20 v1))
(declare-const _9-0 (_ BitVec 9))
(assert (and v11 v21))
(declare-const v22 Bool)
(declare-const _7-0 (_ BitVec 7))
(assert v17)
(declare-const v23 Bool)
(assert (xor v2 (xor v11 v2 v16 (distinct v2 v11 (xor v0 v14 v1) v1 v2 v3 v11 v7 v14 (=> v5 v12) v5) v8 (distinct v2 v11 (xor v0 v14 v1) v1 v2 v3 v11 v7 v14 (=> v5 v12) v5) v16 v8 v2 (distinct v2 v11 (xor v0 v14 v1) v1 v2 v3 v11 v7 v14 (=> v5 v12) v5)) (xor v0 v14 v1) v4 v21 (=> (and v18 v8 v16 v15) v7) v6 v22 v23))
(push)
(assert (= (bvule (bvnand #x89 #x89) #x89) v14 v1 v15 v16 (or v6 (xor v2 (xor v11 v2 v16 (distinct v2 v11 (xor v0 v14 v1) v1 v2 v3 v11 v7 v14 (=> v5 v12) v5) v8 (distinct v2 v11 (xor v0 v14 v1) v1 v2 v3 v11 v7 v14 (=> v5 v12) v5) v16 v8 v2 (distinct v2 v11 (xor v0 v14 v1) v1 v2 v3 v11 v7 v14 (=> v5 v12) v5)) (xor v0 v14 v1) v4 v21 (=> (and v18 v8 v16 v15) v7) v6 v22 v23) v17 (=> v20 v1)) v7 v7))
(pop)
(check-sat)
